g:OGrp, a, b:|g|. (a  b)  (e  (b * (~(a)))) 

latex

Up	groups 1
Definitions of Statement	IMonoid, Mon, IAbMonoid, AbMon, IGroup, OCMon, OGrp
Definitions	t  T, x:A. B(x), IGroup, IMonoid, IAbMonoid, True, T, P & Q, P  Q, , P  Q, x f y, P  Q, Mon, AbMon, OCMon, OGrp
Lemmas	ocgrp wf, grp car wf, inverse wf, grp inverse, comm wf, monoid p wf, abmonoid comm, grp sig wf, true wf, squash wf, iff wf, grp leq op l, grp id wf, grp inv wf, grp op wf, grp leq wf, iff functionality wrt iff